'''
Created on 2011-04-09

@author: kacper
'''
from xml.dom import NotFoundErr


class Formula(object):
#    __slots__ =('FOformula')
    def __init__(self):
        self.FOformula = 1
        
    def prt(self,spec=0):
        pass

    def negFormula(self):
        pass

    def removeThen(self):
        return self
    
    def __str__(self):
        return self.prt()
    
    def __repr__(self):
        return self.prt()
    
    def __cmp__(self, other):
        if  self.prt().__eq__(other.prt()):
            return 0
        if  self.prt().__le__(other.prt()):
            return -1
        return 1
        
        
    
    def __eq__(self,other):
        return self.prt() == str(other)
    
    def __hash__(self):
        return self.prt().__hash__()
    
    def pushNeg(self):
        return self
    
    def getVariables(self):
        return []
    
    def getConsts(self):
        return []
    
    def substitute(self, variable, const): 
        return self;
    
class BinFormula( Formula ):
    #formulas
#    __slots__=("f1","f2","FOformula")
    def prt(self,spec=0):
        pass
    
    def getVariables(self):
        return list(set(self.f1.getVariables() + self.f2.getVariables()))
    
    def getConsts(self):
        return list(set(self.f1.getConsts() + self.f2.getConsts()))
    
    def __init__( self,f1, f2 ):
        super(BinFormula,self).__init__()
        self.f1 = f1
        self.f2 = f2

    def negFormula(self):
        pass
    
    def removeThen(self):
        self.f1 =self.f1.removeThen()
        self.f2 =self.f2.removeThen()
        return self

    def pushNeg(self):
        self.f1 =self.f1.pushNeg()
        self.f2 =self.f2.pushNeg()
        return self

    def substitute(self, variable, const):
        self.f1= self.f1.substitute(variable, const)
        self.f2 =self.f2.substitute(variable, const)
        return self
        
class Default( BinFormula ):    
    def prt(self,spec=0):
        return self.f1.prt(spec) + " => " + self.f2.prt(spec)

    def __init__(self,f1,f2):
        super(Default,self).__init__(f1,f2)
        self.FOformula =0
        
    def negFormula(self):
        return Default(self.f1.negFormula(),self.f2.negFormula())
        
    
class AndFormula( BinFormula ):
    def __init__( self,f1, f2 ):
        super(AndFormula,self).__init__(f1,f2)
    
    def prt(self,spec=0):
        return " ( " + self.f1.prt(spec) + " && " + self.f2.prt(spec) +" ) "

    def negFormula(self):
        return OrFormula(self.f1.negFormula(), self.f2.negFormula() )

class OrFormula( BinFormula ):
    def __init__( self,f1, f2 ):
        super(OrFormula,self).__init__(f1,f2)
    
    def prt(self,spec=0):
        return " ( " + self.f1.prt(spec) + " || " + self.f2.prt(spec) + " ) "

    def negFormula(self):
        return AndFormula(self.f1.negFormula(), self.f2.negFormula() )


class ThenFormula( BinFormula ):
    def __init__( self,f1, f2 ):
        super(ThenFormula,self).__init__(f1,f2)
    def prt(self,spec=0):
        return " ( " +self.f1.prt(spec) + " -> " + self.f2.prt(spec) + " ) "

    def negFormula(self):
        return AndFormula(self.f1, self.f2.negFormula())

    def removeThen(self):
        x = super(ThenFormula,self).removeThen()
        return OrFormula( NotFormula( x.f1), x.f2)
        

class NotFormula(Formula):
#    __slots__ = ("f1")
    def __init__( self,f1):
        super(NotFormula,self).__init__()
        self.f1 = f1
    def prt(self,spec=0):
        return "~" + self.f1.prt(spec)
    
    def negFormula(self):
        return self.f1

    def removeThen(self):
        self.f1 = self.f1.removeThen()
        return self

    def pushNeg(self):
        
        tmp_form = self
        while (isinstance(tmp_form, NotFormula) 
               and isinstance(tmp_form.f1, NotFormula)):
            tmp_form = tmp_form.f1.f1
            
        if not isinstance(tmp_form, NotFormula):
            return tmp_form.pushNeg() 
              
        if (isinstance(tmp_form.f1, AtomicFormula) or
            isinstance(tmp_form.f1, Term) ) :
                return tmp_form
        
        return self.f1.negFormula().pushNeg()
    
    def getVariables(self):
        return self.f1.getVariables()
    
    def getConsts(self):
        return self.f1.getConsts()

    def substitute(self, variable, const):
        self.f1 = self.f1.substitute(variable, const)
        return self
#atomic formulas

class AtomicFormula(Formula):
#    __slots__=("FOformula")
    FOformula = 1
    def prt(self,spec=0):
        pass

    def negFormula(self):
        return NotFormula(self)
    
    


class Relation(AtomicFormula):
#    __slots__ = ("args","_nargs")
    
    def __init__(self,args):
        self.args= args
        self.FOformula = 1
        
    def prt(self,spec=0):
        lst = [x.prt(spec) for x in self.args ]
        lst = map( lambda x:x+",",lst)
        lst = "".join(lst)[0:-1]
        return self.__class__.__name__ + "(" +lst + ")"

    def pushNeg(self):
            return self
        
    def getVariables(self):
        listVars =[]
        for x in self.args:
            listVars += x.getVariables()
        return listVars
    
    def getConsts(self):
        listConsts = []
        for x in self.args:
            listConsts += x.getConsts()
        return listConsts

    def substitute(self, variable, const):
        self.args = map(lambda x: x.substitute(variable, const),self.args )
        return self

class Pin(AtomicFormula):
    def prt(self,spec=0):
        pass


class Eq(AtomicFormula):

    
    def __init__(self,t1,t2):
        self.t1=t1
        self.t2=t2
        self.FOformula = 1

    def prt(self,spec=0):
        return self.t1.prt(spec) + " = " + self.t2.prt(spec)

_dic = {}

 

class RelFac(type):
        
    def __new__(cls, name, bases, dct):
        bases = (Relation,object)
        th_id = dct["th_id"]
        if not ( (name,th_id) in _dic):
            _dic[(name,th_id)] =  type.__new__(cls, name, bases, dct)
            _dic[(name,th_id)]._nargs = dct["nargs"]
        if _dic[(name,th_id)]._nargs != dct["nargs"]:
            raise Exception("wrong number of arguments while constructing "+name)
        return _dic[(name,th_id)]

    def __init__(cls, name, bases, dct):
        bases = (Relation,object)
        super(RelFac, cls).__init__(name, bases, dct)


#terms

class Term(Formula):
#    __slots__ = ("name","FOformula")

    def __init__(self,name):
        self.name = name
        self.FOformula = 1
        
    def prt(self, spec=0):
        return self.name
    
    def negFormula(self):
        return NotFormula(self)

    def pushNeg(self):
        return self

class Const(Term):
    def prt(self, spec=0):
        if spec == 1:
            return self.name + "()" 
        return self.name

    def getConsts(self):
        return [self]

class Var(Term):
    pass

    def getVariables(self):
        return [self]
    
    def substitute(self, variable, const):
        if variable == self:
            return const
        return self